$\forall$$T$:Type, $x$,$y$:$T$. l\_before($x$; $y$; []; $T$) $\Leftarrow\!\Rightarrow$ False